b:, x:Top. if b then x else x fi  ~ x 

latex

Definitions	x:A. B(x), if b then t else f fi , t  T, P  Q, tt, ff, , , Unit, P  Q, P & Q,
Lemmas	bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, top wf